compare atoe-tcsZ.tex atoe-tcsJG.tex
File #1: atoe-tcsZ.tex
File #2: atoe-tcsJG.tex

Nonmatching lines (File "atoe-tcsZ.tex"; Line 690:697; File "atoe-tcsJG.tex"; Line 690:697)
 690	\cdot     &\rTo    &  \cdot    &\rTo    &\cdot  &\rTo        & \cdot &\rTo
 691	& \cdot\\
 692	\dTo   &        &\dTo   &        & \dTo    &  & \dTo  &  & \dTo  \\
 693	\cdot   &\rTo  & \cdot & \rTo  & \cdot &\rTo & \cdot &\rTo   & \cdot \\
 694	\dTo  & &\dTo  & & \dTo & & \dTo & &\dTo  \\
 695	\cdot  &\rTo & \cdot &\rTo  &\cdot  & \rTo   & \cdot &\rTo   & \cdot\\
 696	\dTo   &       &\dTo  &       & \dTo  &      & \dTo & &\dTo \\
 697	\cdot     &\rTo  & \cdot     &\rTo  &\cdot  & \rTo    & \cdot &\rTo   & \cdot\\

 690	\cdot     &\rOnto    &  \cdot    &\rOnto    &\cdot  &\rOnto        & \cdot &\rOnto
 691	& \cdot\\
 692	\dOnto   &        &\dOnto   &        & \dOnto    &  & \dOnto  &  & \dOnto  \\
 693	\cdot   &\rOnto  & \cdot & \rOnto  & \cdot &\rOnto & \cdot &\rOnto   & \cdot \\
 694	\dOnto  & &\dOnto  & & \dOnto & & \dOnto & &\dOnto  \\
 695	\cdot  &\rOnto & \cdot &\rOnto  &\cdot  & \rOnto   & \cdot &\rOnto   & \cdot\\
 696	\dOnto   &       &\dOnto  &       & \dOnto  &      & \dOnto & &\dOnto \\
 697	\cdot     &\rOnto  & \cdot     &\rOnto  &\cdot  & \rOnto    & \cdot &\rOnto   & \cdot\\


Nonmatching lines (File "atoe-tcsZ.tex"; Line 721:722; File "atoe-tcsJG.tex"; Line 721:722)
 721	be sound!) \emph{Klop's commutative diagrams} can be used
 722	instead~\cite{[Kl.CRS]}. Klop's diagrams are constructed using

 721	be sound!) Klop's \emph{commutative diagrams} can be used
 722	instead~\cite{[Kl.CRS]}. Klop diagrams are constructed using


Nonmatching lines (File "atoe-tcsZ.tex"; Line 736; File "atoe-tcsJG.tex"; Line 736)
 736	sets of redexes. Both multi-step and Klop's diagrams use empty (multi-)

 736	sets of redexes. Both multi-step and Klop diagrams use empty (multi-)


Extra lines in 1st before 912 in 2nd (File "atoe-tcsZ.tex"; Line 912; File "atoe-tcsJG.tex"; Line 912)
 912	


Nonmatching lines (File "atoe-tcsZ.tex"; Line 948:949; File "atoe-tcsJG.tex"; Line 947:948)
 948	\item[(3)] We call a stable set $\stab$ \emph{regular} if in no term an
 949	$\stab$-unneeded redex can duplicate an $\stab$-needed one.

 947	\item[(3)] We call a stable set $\stab$ \emph{regular} if in no term can
 948	an $\stab$-unneeded redex duplicate an $\stab$-needed one.


Nonmatching lines (File "atoe-tcsZ.tex"; Line 1012:1013; File "atoe-tcsJG.tex"; Line 1011:1012)
1012	$\stab$-unneeded; But suppose
1013	$e\not\in \stab$. Since $u$ is $\stab$-unneeded, there is an

1011	$\stab$-unneeded. But suppose
1012	$e\not\in \stab$: Since $u$ is $\stab$-unneeded, there is an


Extra lines in 1st before 1245 in 2nd (File "atoe-tcsZ.tex"; Line 1246:1249; File "atoe-tcsJG.tex"; Line 1245)
1246	
1247	{My checking stops here so far...}
1248	
1249	


Nonmatching lines (File "atoe-tcsZ.tex"; Line 1262; File "atoe-tcsJG.tex"; Line 1257)
1262	family relation needed to develop an abstract theory of optimal

1257	a family relation needed to develop an abstract theory of optimal


Extra lines in 2nd before 1268 in 1st (File "atoe-tcsZ.tex"; Line 1268; File "atoe-tcsJG.tex"; Line 1263)
1263	the family relation


Nonmatching lines (File "atoe-tcsZ.tex"; Line 1322:1324; File "atoe-tcsJG.tex"; Line 1318:1320)
1322	we want to be as general as (reasonably) possible, here we do not
1323	investigate any further finer axiomatizations of the residual relation that
1324	would imply [FFD]. The reason for considering more notions of family than

1318	we want to be as general as (reasonably) possible, we do not
1319	investigate here any finer axiomatization of the residual relation that
1320	would imply [FFD]. The reason for considering notions of family other than


Nonmatching lines (File "atoe-tcsZ.tex"; Line 1330; File "atoe-tcsJG.tex"; Line 1326)
1330	the nice property of (de)compositionality, facilitating study of complex

1326	the nice property of compositionality, facilitating study of complex


Nonmatching lines (File "atoe-tcsZ.tex"; Line 1350; File "atoe-tcsJG.tex"; Line 1346)
1350	of possibly completely unrelated graphically equal subterms), it is

1346	of possibly completely unrelated, but graphically equal, subterms), it is


Nonmatching lines (File "atoe-tcsZ.tex"; Line 1353; File "atoe-tcsJG.tex"; Line 1349)
1353	members of a same family since (by [creation]) they have different

1349	members of the same family since (by [creation]) they have different


Nonmatching lines (File "atoe-tcsZ.tex"; Line 1403; File "atoe-tcsJG.tex"; Line 1399:1400)
1403	residuals of $u$, hence belong to the same family $\phi_u$. Similarly, $v$ and

1399	residuals of $u$, and hence belong to the same family $\phi_u$.
1400	Similarly, $v$ and


Nonmatching lines (File "atoe-tcsZ.tex"; Line 1492; File "atoe-tcsJG.tex"; Line 1489)
1492	orthogonal ERSs, to all DFSs. We now allow for arbitrary

1489	orthogonal ERSs, to all DFSs. In the following we allow for arbitrary


Nonmatching lines (File "atoe-tcsZ.tex"; Line 1545; File "atoe-tcsJG.tex"; Line 1542)
1545	However, it is necessary and sufficient to insure that the set of normal

1542	However, it is necessary and sufficient to ensure that the set of normal


Nonmatching lines (File "atoe-tcsZ.tex"; Line 1603:1605; File "atoe-tcsJG.tex"; Line 1600:1603)
1603	reduction, and to contract safely (without a danger of missing an
1604	$\stab$-normal form whenever it exists) any residual of an $\stab$-needed
1605	redex, even if it is no longer $\stab$-needed.

1600	reduction, and to contract any residual of an $\stab$-needed
1601	redex safely (without the danger of missing an
1602	$\stab$-normal form whenever it exists),
1603	even if the residual is no longer $\stab$-needed.


Nonmatching lines (File "atoe-tcsZ.tex"; Line 1687; File "atoe-tcsJG.tex"; Line 1685)
1687	$\stab$-optimal in the sense that it has a minimal number of

1685	$\stab$-optimal in the sense that it has the minimal number of


Extra lines in 1st before 1703 in 2nd (File "atoe-tcsZ.tex"; Line 1705; File "atoe-tcsJG.tex"; Line 1703)
1705	


Extra lines in 2nd before 1709 in 1st (File "atoe-tcsZ.tex"; Line 1709; File "atoe-tcsJG.tex"; Line 1706)
1706	\john{We have not introduced ASDRSs.}


Nonmatching lines (File "atoe-tcsZ.tex"; Line 1716; File "atoe-tcsJG.tex"; Line 1714)
1716	family of $v$. \footnote{The extraction process was thought to require the

1714	family of $v$.\footnote{The extraction process was thought to require the


Nonmatching lines (File "atoe-tcsZ.tex"; Line 1728; File "atoe-tcsJG.tex"; Line 1726)
1728	decidability of the family relation. For higher order rewrite systems whose

1726	decidability of the family relation. For higher order rewrite systems, whose


Nonmatching lines (File "atoe-tcsZ.tex"; Line 1743:1744; File "atoe-tcsJG.tex"; Line 1741:1742)
1743	are viewed to belong
1744	to the same family, as labels of such redexes are the same. Such redexes

1741	are viewed as belonging
1742	to the same family, as the labels of such redexes are the same. Such redexes


Nonmatching lines (File "atoe-tcsZ.tex"; Line 1769:1771; File "atoe-tcsJG.tex"; Line 1767:1770)
1769	any nesting relation imposed on redexes, unlike in ARSs~\cite{[GLM]}, and
1770	there is no concept of `left' or `right' occurrences in DRSs. However, our
1771	concept of standardization captures the essence of the usual one in many

1767	any nesting relation imposed on redexes, unlike in the ARSs
1768	of~\cite{[GLM]}, and
1769	there is no concept of `left' or `right' occurrences in DRSs. However, our
1770	concept of standardization captures the essence of the usual notion in many


Nonmatching lines (File "atoe-tcsZ.tex"; Line 1777; File "atoe-tcsJG.tex"; Line 1776)
1777	theory' of standardization in ARSs with axiomatized nesting relation,

1776	theory' of standardization in ARSs with an axiomatized nesting relation,


Nonmatching lines (File "atoe-tcsZ.tex"; Line 2109; File "atoe-tcsJG.tex"; Line 2108)
2109	relation $\extr$ is trivially strongly normalizing, and in order to proof

2108	relation $\extr$ is trivially strongly normalizing, and in order to prove


Nonmatching lines (File "atoe-tcsZ.tex"; Line 2349; File "atoe-tcsJG.tex"; Line 2348)
2349	$P'_1$), therefore can be permuted with its next step. That $w$-step is

2348	$P'_1$), therefore it can be permuted with its next step. That $w$-step is


Nonmatching lines (File "atoe-tcsZ.tex"; Line 2377:2378; File "atoe-tcsJG.tex"; Line 2376)
2377	
2378	

2376	\john{Checked to here now.}


Nonmatching lines (File "atoe-tcsZ.tex"; Line 2465; File "atoe-tcsJG.tex"; Line 2463)
2465	labells in Levy's labelling system for the \lc, and cannot be related

2463	labels in Levy's labelling system for the \lc, and cannot be related


*** EOF on both files at the same time ***
